Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.


QTRS
  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS
  ↳ Non-Overlap Check
QTRS
      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)


Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
QDP
          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF33(store, m, false) -> SNDSPLIT2(m, app2(map_f2(self, nil), store))
PROCESS2(store, m) -> LENGTH1(store)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> APP2(map_f2(self, nil), sndsplit2(m, store))
IF13(store, m, true) -> FSTSPLIT2(m, store)
IF23(store, m, false) -> MAP_F2(self, nil)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF13(store, m, true) -> EMPTY1(fstsplit2(m, store))
PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF33(store, m, false) -> APP2(map_f2(self, nil), store)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))
IF13(store, m, false) -> MAP_F2(self, nil)
IF13(store, m, false) -> FSTSPLIT2(m, app2(map_f2(self, nil), store))
IF13(store, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(self, nil), store)))
APP2(cons2(h, t), x) -> APP2(t, x)
IF33(store, m, false) -> MAP_F2(self, nil)
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF23(store, m, false) -> SNDSPLIT2(m, store)
PROCESS2(store, m) -> LEQ2(m, length1(store))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF13(store, m, false) -> APP2(map_f2(self, nil), store)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 7 SCCs with 15 less nodes.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP2(cons2(h, t), x) -> APP2(t, x)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


APP2(cons2(h, t), x) -> APP2(t, x)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
APP2(x1, x2)  =  APP1(x1)
cons2(x1, x2)  =  cons1(x2)

Lexicographic Path Order [19].
Precedence:
[APP1, cons1]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
MAP_F2(x1, x2)  =  MAP_F1(x2)
cons2(x1, x2)  =  cons1(x2)

Lexicographic Path Order [19].
Precedence:
[MAPF1, cons1]


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LENGTH1(cons2(h, t)) -> LENGTH1(t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


LENGTH1(cons2(h, t)) -> LENGTH1(t)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
LENGTH1(x1)  =  LENGTH1(x1)
cons2(x1, x2)  =  cons2(x1, x2)

Lexicographic Path Order [19].
Precedence:
cons2 > LENGTH1


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LEQ2(s1(n), s1(m)) -> LEQ2(n, m)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
LEQ2(x1, x2)  =  LEQ1(x1)
s1(x1)  =  s1(x1)

Lexicographic Path Order [19].
Precedence:
trivial


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
SNDSPLIT2(x1, x2)  =  x1
s1(x1)  =  s1(x1)
cons2(x1, x2)  =  x1

Lexicographic Path Order [19].
Precedence:
trivial


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].


The following pairs can be strictly oriented and are deleted.


FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
The remaining pairs can at least by weakly be oriented.
none
Used ordering: Combined order from the following AFS and order.
FSTSPLIT2(x1, x2)  =  x1
s1(x1)  =  s1(x1)
cons2(x1, x2)  =  x1

Lexicographic Path Order [19].
Precedence:
trivial


The following usable rules [14] were oriented: none



↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
                ↳ QDPOrderProof
QDP
                    ↳ PisEmptyProof
              ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ Non-Overlap Check
    ↳ QTRS
      ↳ DependencyPairsProof
        ↳ QDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP

Q DP problem:
The TRS P consists of the following rules:

PROCESS2(store, m) -> IF13(store, m, leq2(m, length1(store)))
IF13(store, m, false) -> IF33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
IF33(store, m, false) -> PROCESS2(sndsplit2(m, app2(map_f2(self, nil), store)), m)
IF23(store, m, false) -> PROCESS2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
IF13(store, m, true) -> IF23(store, m, empty1(fstsplit2(m, store)))

The TRS R consists of the following rules:

fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
process2(store, m) -> if13(store, m, leq2(m, length1(store)))
if13(store, m, true) -> if23(store, m, empty1(fstsplit2(m, store)))
if13(store, m, false) -> if33(store, m, empty1(fstsplit2(m, app2(map_f2(self, nil), store))))
if23(store, m, false) -> process2(app2(map_f2(self, nil), sndsplit2(m, store)), m)
if33(store, m, false) -> process2(sndsplit2(m, app2(map_f2(self, nil), store)), m)

The set Q consists of the following terms:

fstsplit2(0, x0)
fstsplit2(s1(x0), nil)
fstsplit2(s1(x0), cons2(x1, x2))
sndsplit2(0, x0)
sndsplit2(s1(x0), nil)
sndsplit2(s1(x0), cons2(x1, x2))
empty1(nil)
empty1(cons2(x0, x1))
leq2(0, x0)
leq2(s1(x0), 0)
leq2(s1(x0), s1(x1))
length1(nil)
length1(cons2(x0, x1))
app2(nil, x0)
app2(cons2(x0, x1), x2)
map_f2(x0, nil)
map_f2(x0, cons2(x1, x2))
process2(x0, x1)
if13(x0, x1, true)
if13(x0, x1, false)
if23(x0, x1, false)
if33(x0, x1, false)

We have to consider all minimal (P,Q,R)-chains.